X, Y:ik:LocKnd fp Top, ik:LocKnd.
ik  dom(interface-union(X;Y)) ~ (ik  dom(X) ik  dom(Y)) 

latex

Definitions	t  T, LocKnd, type List, Top, x:A. B(x), (x  l), {x:A| B(x)} , x:AB(x), x.A(x), x. t(x), t.1, locknd-deq(), deq-member(eq;x;L), b, Type, , left + right, P  Q, as @ bs, p q, P  Q, P  Q, x:A  B(x), P & Q, P  Q, <a, b>, , s = t, {T}, SQType(T), s ~ t, fpf-domain(f), x  dom(f), interface-union(X;Y), a:A fp B(a)
Lemmas	member append, bool sq, iff imp equal bool, iff functionality wrt iff, iff transitivity, assert of bor, or functionality wrt iff, assert-deq-member, bor wf, append wf, assert wf, deq-member wf, locknd-deq wf, pi1 wf, l member wf, top wf, LocKnd wf